\begin{tabbing}
es{-}sends{-}iff(${\it es}$;$l$;${\it tgs}$;${\it da}$;${\it ds}$;$e$.$f$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex]($\uparrow$es{-}isrcv(${\it es}$; $e$))
\\[0ex]$\Rightarrow$ (es{-}lnk(${\it es}$; $e$) = $l$ $\in$ IdLnk)
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex](($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))
\\[0ex]c$\wedge$ \=((es{-}lnk(${\it es}$; ${\it e'}$) = $l$ $\in$ IdLnk)\+
\\[0ex]$\wedge$ (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$ $\in$ Id)
\\[0ex]$\wedge$ (es{-}sender(${\it es}$; ${\it e'}$) = es{-}sender(${\it es}$; $e$) $\in$ es{-}E(${\it es}$)))))
\-\-\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; $e$) $\in$ ${\it tgs}$ $\in$ Id))
\\[0ex]c$\wedge$ \=(($\forall$${\it e'}$:es{-}E(${\it es}$). \+
\\[0ex]($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))
\\[0ex]$\Rightarrow$ (es{-}lnk(${\it es}$; ${\it e'}$) = $l$ $\in$ IdLnk)
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$ $\in$ Id)
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; ${\it e'}$); fpf{-}cap(${\it da}$; Kind{-}deq; es{-}kind(${\it es}$; ${\it e'}$); void)))
\\[0ex]$\wedge$ ($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; source($l$); $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top))))
\-\\[0ex]c$\wedge$ \=(alle{-}at(\=${\it es}$;\+\+
\\[0ex]source($l$);
\\[0ex]$e$.($\forall$$i$:int\_seg(0; $\parallel$$f$($e$)$\parallel$). 
\\[0ex]$\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex](($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; ${\it e'}$) = $l$ $\in$ IdLnk)
\\[0ex]$\wedge$ (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$ $\in$ Id)
\\[0ex]$\wedge$ (es{-}sender(${\it es}$; ${\it e'}$) = $e$ $\in$ es{-}E(${\it es}$))
\\[0ex]$\wedge$ (es{-}index(${\it es}$; ${\it e'}$) = $i$ $\in$ $\mathbb{Z}$))))
\-\-\\[0ex]$\wedge$ \=($\forall$${\it e'}$:es{-}E(${\it es}$). \+
\\[0ex]($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))
\\[0ex]$\Rightarrow$ (es{-}lnk(${\it es}$; ${\it e'}$) = $l$ $\in$ IdLnk)
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$ $\in$ Id)
\\[0ex]$\Rightarrow$ \=((es{-}index(${\it es}$; ${\it e'}$) $<$ $\parallel$$f$(es{-}sender(${\it es}$; ${\it e'}$))$\parallel$)\+
\\[0ex]c$\wedge$ (\=$<$es{-}tag(${\it es}$; ${\it e'}$), es{-}val(${\it es}$; ${\it e'}$)$>$\+
\\[0ex]=
\\[0ex]$f$(es{-}sender(${\it es}$; ${\it e'}$))[es{-}index(${\it es}$; ${\it e'}$)]
\\[0ex]$\in$ (${\it tg}$:Id $\times$ fpf{-}cap(${\it da}$; Kind{-}deq; rcv($l$,${\it tg}$); void))))))
\-\-\-\-\-
\end{tabbing}